a:{...0}, n:{...-1}. (a rem n) = (-((-a) rem -n)) 

latex

Up	int 2, int 2
Definitions	t  T, x:A. B(x), P & Q, False, P  Q, A, a  b  T , , P  Q, P  Q, , A  B, {...i}
Lemmas	int lower wf, minus functionality wrt eq, nequal wf, rem to div, div 3 to 1